COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	match.lsp[f81,jmc]	ekl version of problem with match and sublis
C00005 ENDMK
C⊗;
match.lsp[f81,jmc]	ekl version of problem with match and sublis

(decl match1 |ground⊗ground → ground| constant)
(decl isvar |ground → truthval| constant)
(decl sublis |ground⊗ground → ground| constant)

(decl (NO error) ground constant)
(decl (pat exp) ground)
(decl fix |ground→ground| constant)

(axiom |∀pat exp.match1(pat,exp) =
if atom pat then (if isvar pat then list(cons(pat,exp))
else if pat = exp then nil else list(NO))
else if atom exp then list(NO)
else fix(match1(car pat,car exp) * match1(cdr pat, cdr exp))|)

(axiom |∀u.fix(u) = if null u then nil
else if member(NO,u) then list(NO)
else (λz.if null z then cons(car u, fix(cdr u))
else if cdr z = cdar u then fix(cdr u)
else list(NO))(assoc(car u,cdr u))|)

(axiom |∀pat exp. sublis(pat,exp) = if atom pat
then (if isvar pat then (λz.if null z then error else cdr z)(assoc pat alist)
else pat) else cons(sublis(car pat,alist),sublis(cdr pat,alist))|)


;;; A better match would use QUOTE for subexpressions without variables.
;;; We have

(axiom |∀pat exp a.match(pat,exp,a) =
	 	if a = 'NO then 'NO
		else if atom pat then
		 (λx. 	if null x then cons(cons(pat,exp),a)
			 else if exp = cdr x then a
			else 'NO)
		 (assoc(pat,a))
		else if car pat = 'QUOTE then (if cadr pat = e then a else 'NO)
		else if atom e then 'NO
		else match(car pat,car exp,match(cdr pat,cdr exp,a))|)

(axiom |∀pat a.sublis(pat,a) =
		if atom pat then cdr assoc(pat,a)
		else if a pat = 'QUOTE then cadr pat
		else cons(sublis(car pat,a), sublis(cdr pat,a))|)

;;; The theorem is then
;;; ∀pat exp a.match(pat,exp,a) ≠ 'NO ⊃ sublis(pat,match(pat,exp,a))= exp